A, B:Type, L2:(Id(AB(Top List))) List, L:(TopIdTop) List, tg:Id, a:A, b:B.
{map(x.2of(x);L) = concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(a,b));L2))  (IdTop) List
{ (tg  map(p.1of(p);L2))
{ filter(ms.1of(2of(ms)) = tg;L) = nil  (TopIdTop) List} 

latex

Definitions	x:A. B(x), {T}, Prop, concat(ll), map(f;as), P  Q, P & Q, P  Q, filter(P;l), a = b, 1of(t), 2of(t), x. t(x), t  T, (x  l), Id, Top, x:A. B(x), A, P  Q, False
Lemmas	l member wf, pi2 wf, pi1 wf, eq id wf, filter wf, nil-iff-no-member, top wf, Id wf, map wf, concat wf, not wf, member filter, assert-eq-id, member map, member-concat